Nuprl Lemma : p-first-append
11,40
postcript
pdf
A
,
B
:Type,
L1
,
L2
:((
A
(
B
+ Top)) List).
p-first(
L1
@
L2
) = p-first([p-first(
L1
); p-first(
L2
)])
A
(
B
+ Top)
latex
Definitions
Top
,
left
+
right
,
x
:
A
B
(
x
)
,
type
List
,
[]
,
t
T
,
x
:
A
.
B
(
x
)
,
p-first(
L
)
,
[
car
/
cdr
]
,
as
@
bs
,
s
=
t
,
Type
,
Void
,
x
:
A
.
B
(
x
)
,
S
T
,
x
,
y
.
t
(
x
;
y
)
,
P
Q
,
inl
x
,
inr
x
,
True
,
T
,
list_accum(
x
,
a
.
f
(
x
;
a
);
y
;
l
)
Lemmas
equal-top
,
list
accum
wf
,
list
accum
append
,
top
wf
,
append
wf
,
p-first
wf
origin
A, B:Type, L1, L2:((A
(B + Top)) List).
A(B + Top) A, B:Type, L1, L2:((A(B + Top)) List).
A(B + Top) B(x) Tx:A. B(x)
x:A.B(x)
T
x,y. t(x;y)
Q
T